%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Task
%CreateTask\_T
%DeleteTask\_T
%ExecuteRunningTask\_T
%SuspendTask\_T
%ResumeTask\_T
%ChangeTaskPriority\_T
%Migration\_T
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[a4paper, 12pt]{article}

\usepackage[margin=2cm, includeheadfoot]{geometry}
\usepackage{z-eves}

\makeatletter
\renewcommand{\@znoskip}{\offinterlineskip}
\makeatother

\begin{document}

%\begin{zsection}
%  \SECTION m6Task \parents standard\_toolkit
%\end{zsection}

\begin{zed}
  [CONTEXT, TASK, CORE]
\end{zed}

\begin{axdef}
  bare\_context: CONTEXT\\
  idles: \finset TASK\\
  cores: \finset CORE
\where
  \# cores = \# idles
\end{axdef}

\begin{zproof}[unnamed\$n3\$domainCheck]
 prove; 
\end{zproof}


\begin{zed}
STATE ::= nonexistent | ready | blocked | suspended | running
\end{zed}

\begin{zed}
% \begin[disabled]{zed}
transition == (\{blocked\} \cross  \{nonexistent, ready, running, suspended\})\\
               \t1 \cup  (\{nonexistent\} \cross  \{ready, running\})\\
               \t1 \cup  (\{ready\} \cross  \{nonexistent, running, suspended\})\\
               \t1 \cup  (\{running\} \cross  \{blocked, nonexistent, ready, suspended\})\\
               \t1 \cup  (\{suspended\} \cross  \{nonexistent, ready, running\})
\end{zed}

\begin{schema}{TaskData}
  tasks: \finset TASK \\
  running\_task: TASK \\
  idle: TASK
\where
  running\_task \in tasks \\
  idle \in tasks \\
  idle \in idles
\end{schema}

\begin{schema}{Init\_TaskData}
  TaskData~'
\where
  tasks' = \{idle'\} \\
  running\_task' = idle' \\
  idle' \in idles
\end{schema}

\begin{schema}{StateData}
  state: TASK \fun STATE
\end{schema}

\begin{schema}{ContextData}
  phys\_context: CONTEXT \\
  log\_context: TASK \fun CONTEXT
\end{schema}

\begin{schema}{Init\_ContextData}
  ContextData~'
\where
  phys\_context' = bare\_context \\
  log\_context' = (\lambda x: TASK @ bare\_context)
\end{schema}

\begin{schema}{PrioData}
  priority: TASK \fun \nat
\where
  \forall i: idles @ priority(i) = 0
\end{schema}

\begin{schema}{Init\_PrioData}
  PrioData~'
\where
  priority' = (\lambda x: TASK @ 0)
\end{schema}

\begin{schema}{Task}
  TaskData \\
  StateData \\
  ContextData \\
  PrioData
\where
  tasks = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg )\\
  state \inv  \limg  \{running\} \rimg  = \{running\_task\}\\
  \forall  pt: state \inv  \limg  \{ready\} \rimg  @ priority(running\_task) \geq  priority(pt)
\end{schema}

\begin{schema}{\Delta Task}
  Task \\
  Task~'
\where
  \forall st: TASK | state'(st) \neq state(st) @ state(st) \mapsto state'(st) \in transition \\
  idle' = idle
\end{schema}

\begin{schema}{Init\_Task}
  Task~'
\where
  Init\_TaskData \\
  state' = (\lambda x: TASK @ nonexistent) \oplus \{(idle' \mapsto running)\} \\
  Init\_ContextData \\
  Init\_PrioData
\end{schema}

\begin{schema}{Reschedule}
  \Delta Task \\
  target?: TASK \\
  tasks?: \power TASK \\
  st?: STATE \\
  pri?: TASK \fun \nat
\where
  tasks' = tasks? \\
  running\_task' = target? \\
  state' = state \oplus \{(target? \mapsto running), (running\_task \mapsto st?)\} \\
  phys\_context' = log\_context(target?) \\
  log\_context' = log\_context \oplus \{(running\_task \mapsto phys\_context)\} \\
  priority' = pri?
\end{schema}


\begin{schema}{CreateTaskN\_T}
  \Delta Task \\
  target?: TASK \\
  newpri?: \nat
\where
  state(target?) = nonexistent \\
  newpri? \leq priority(running\_task) \\
  tasks' = tasks \cup \{target?\} \\
  running\_task' = running\_task \\
  state' = state \oplus \{(target?, ready)\} \\
  \Xi ContextData \\
  priority' = priority \oplus \{(target?, newpri?)\}
\end{schema}

\begin{schema}{CreateTaskS\_T}
  \Delta Task \\
  target?: TASK \\
  newpri?: \nat
\where
  state(target?) = nonexistent \\
  newpri? > priority(running\_task) \\
  \exists st?: STATE; tasks?: \power TASK; pri?: TASK \fun \nat \\
    | st? = ready \land tasks? = tasks \cup \{(target?)\} \\
    \land pri? = priority \oplus \{(target?, newpri?)\} @ Reschedule
\end{schema}

\begin{schema}{DeleteTaskN\_T}
  \Delta Task \\
  target?: TASK \\
  topReady!: TASK
\where
  target? \in tasks \setminus \{ idle \} \\
  state(target?) \in \{ ready, blocked, suspended \} \\
  tasks' = tasks \setminus \{ target? \} \\
  running\_task' = running\_task \\
  state' = state \oplus \{ (target?, nonexistent) \} \\
  phys\_context' = phys\_context \\
  log\_context' = log\_context \oplus \{ (target?, bare\_context) \} \\
  \Xi PrioData \\
  topReady! = running\_task
\end{schema}

\begin{schema}{DeleteTaskS\_T}
  \Delta Task \\
  target?: TASK \\
  topReady!: TASK
\where
  target? \in tasks \setminus \{ idle \} \\
  state(target?) \in \{ running \} \\
  state(topReady!) = ready \\
  \forall t: state \inv \limg \{ ready \} \rimg @ priority(topReady!) \geq priority(t) \\
  tasks' = tasks \setminus \{ target? \} \\
  running\_task' = topReady! \\
  state' = state \oplus \{ (topReady!, running), (target?, nonexistent) \} \\
  phys\_context' = log\_context(topReady!) \\
  log\_context' = log\_context \oplus \{ (target?, bare\_context) \} \\
  \Xi PrioData
\end{schema}

\begin{schema}{SuspendTaskN\_T}
  \Delta Task \\
  target?: TASK \\
  topReady!: TASK
\where
  target? \in tasks \setminus \{ idle \} \\
  state(target?) \in \{ ready, blocked \} \\
  \Xi TaskData \\
  state' = state \oplus \{ (target?, suspended) \} \\
  \Xi ContextData \\
  \Xi PrioData \\
  topReady! = running\_task
\end{schema}

\begin{schema}{SuspendTaskS\_T}
  \Delta Task \\
  target?: TASK \\
  topReady!: TASK
\where
  target? \in tasks \setminus \{ idle \} \\
  state(target?) \in \{ running \} \\
  state(topReady!) = ready \\
  \forall t: state \inv \limg \{ ready \} \rimg @ priority(topReady!) \geq priority(t) \\
  \exists st?: STATE | st? =  suspended @ Reschedule[tasks/tasks?, priority/pri?, topReady!/target?]
\end{schema}

\begin{schema}{SuspendTaskO\_T}
  \Xi Task \\
  target?: TASK \\
  topReady!: TASK
\where
  state(target?) \in \{ suspended \} \\
  topReady! = running\_task
\end{schema}

\begin{schema}{ResumeTaskN\_T}
  \Delta Task \\
  target?: TASK
\where
  state(target?) = suspended \\
  priority(target?) \leq priority(running\_task) \\
  \Xi TaskData \\
  state' = state \oplus \{ (target?, ready) \} \\
  \Xi ContextData \\
  \Xi PrioData
\end{schema}

\begin{schema}{ResumeTaskS\_T}
  \Delta Task \\
  target?: TASK
\where
  state(target?) = suspended \\
  priority(target?) > priority(running\_task) \\
  \exists st?: STATE | st? = ready @ Reschedule[tasks/tasks?, priority/pri?]
\end{schema}

\begin{schema}{ChangeTaskPriorityN\_T}
  \Delta Task \\
  target?: TASK \\
  newpri?: \nat \\
  topReady!: TASK
\where
  state(target?) = ready \implies newpri? \leq priority(running\_task) \\
  state(target?) = running \implies (\forall t: state \inv \limg \{ ready \} \rimg @ newpri? \geq priority(t)) \\
  state(target?) \neq nonexistent \\
  target? = idle \implies newpri? = 0 \\
  \Xi TaskData \\
  \Xi StateData \\
  \Xi ContextData \\
  priority' = priority \oplus \{ (target?, newpri?) \} \\
  topReady! = running\_task
\end{schema}

\begin{schema}{ChangeTaskPriorityS\_T}
  \Delta Task \\
  target?: TASK \\
  newpri?: \nat \\
  topReady!: TASK
\where
  state(target?) = ready \\
  newpri? > priority(running\_task) \\
  target? = idle \implies newpri? = 0 \\
  \exists st?: STATE; pri?: TASK \fun \nat | st? = ready \land pri? = priority \oplus \{ (target?, newpri?) \} @ Reschedule[tasks/tasks?] \\
  topReady! = target?
\end{schema}

\begin{schema}{ChangeTaskPriorityD\_T}
  \Delta Task \\
  target?: TASK \\
  newpri?: \nat \\
  topReady!: TASK
\where
  state(target?) = running \\
  target? = idle \implies newpri? = 0 \\
  state(topReady!) = ready \\
  \forall t: state \inv \limg \{ ready \} \rimg @ priority(topReady!) \geq priority(t) \\
  newpri? < priority(topReady!) \\
  \exists st?: STATE; pri?: TASK \fun \nat | st? = ready \land pri? = priority \oplus \{ (target?,  newpri?) \} @ Reschedule[tasks/tasks?, topReady!/target?]
\end{schema}


\begin{schema}{Multi\_Task}
  subTask: cores \fun Task \\
  exeCore: TASK \psurj cores
\where
  \forall c1, c2: cores | c1 \neq c2 @ \\
    (subTask~c1) . tasks \cap (subTask~c2) . tasks = \emptyset \\
  % Following two predicates are replacement for the third one. They accelerate ProZ animation significantly.
  %\forall t: TASK | (\exists c: cores @ t \in (subTask~(c)) . tasks) @ \\
  %  t \in \dom exeCore
  %\forall t: \dom exeCore @ t \in (subTask~(exeCore~t)) . tasks \\
  \dom exeCore \in \finset TASK \\
  \dom exeCore = \bigcup \{c: cores @ (subTask(c)) . tasks \}
\end{schema}

\begin{zproof}[Multi\_Task\$domainCheck]
 prove; 
\end{zproof}


\begin{schema}{Init}
  Multi\_Task~'
\where
  \dom exeCore' = idles \\
  \forall c: cores @ \exists Task~'
    | Init\_Task @ subTask'(c) = \theta Task~'
      \land exeCore'((subTask'(c)) . idle) = c
\end{schema}

\begin{zproof}[Init\$domainCheck]
 prove by reduce; 
\end{zproof}

\begin{schema}{PromoteC}
  \Delta Multi\_Task \\
  \Delta Task \\
  target?: TASK \\
  executeCore: cores
\where
  target? \notin \dom exeCore \\
  subTask(executeCore) = \theta Task \\
  subTask' = subTask \oplus \{ (executeCore, \theta Task~') \} \\
  exeCore' = exeCore \oplus \{ (target?, executeCore) \}
\end{schema}

\begin{zproof}[PromoteC\$domainCheck]
 prove; 
\end{zproof}

\begin{zed}
  createTaskN\_MT \defs \exists \Delta Task @ CreateTaskN\_T \land PromoteC
\end{zed}

\begin{zed}
  createTaskS\_MT \defs \exists \Delta Task @ CreateTaskS\_T \land PromoteC
\end{zed}

\begin{schema}{findACore\_MT}
  Multi\_Task \\
  target?: TASK \\
  newpri?: \nat \\
  executeCore?: CORE \\
  executeCore: CORE
\where
  executeCore? \notin cores \\
  executeCore \in cores \\
  \exists tcs, cs: \finset cores \\
    | tcs = \{~pc: cores; subS: Task \\
      | subS = subTask(pc) \\
        \land newpri? > subS . priority (subS . running\_task) @ pc ~\} \\
    @ (tcs = \emptyset \implies cs = cores) \\
      \land (tcs \neq \emptyset \implies cs = tcs) \\
      \land (\forall oc: cs @ executeCore \in cs \\
        \land \# (exeCore \inv \limg \{executeCore\} \rimg) \leq \\
          \# (exeCore \inv \limg \{oc\} \rimg))
\end{schema}

\begin{zproof}[findACore\_MT\$domainCheck]
 prove by reduce; 
 use applyInRanFun[cores, Task][f:=subTask, a:=pc]; 
 apply Task\$member to predicate subTask~pc \in Task;
 prove;
\end{zproof}

\begin{zed}
  CreateTaskN\_MT \defs ([executeCore?, executeCore: CORE\\
    \t1 | executeCore? \in cores \land executeCore = executeCore?] \lor findACore\_MT) \land createTaskN\_MT
\end{zed}

\begin{zed}
  CreateTaskS\_MT \defs ([executeCore?, executeCore: CORE\\
    \t1 | executeCore? \in cores \land executeCore = executeCore?] \lor findACore\_MT) \land createTaskS\_MT
\end{zed}

\begin{schema}{PromoteD}
  \Delta Multi\_Task \\
  \Delta Task \\
  target?: TASK
\where
  target? \in \dom exeCore \\
  subTask(exeCore(target?)) = \theta Task \\
  subTask' = subTask \oplus \{ (exeCore(target?), \theta Task~') \} \\
  exeCore' = \{ target? \} \ndres exeCore
\end{schema}

\begin{zproof}[PromoteD\$domainCheck]
 prove; 
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 prove;
\end{zproof}


\begin{zed}
  DeleteTaskN\_MT \defs \exists \Delta Task @ DeleteTaskN\_T \land PromoteD
\end{zed}

\begin{zed}
  DeleteTaskS\_MT \defs \exists \Delta Task @ DeleteTaskS\_T \land PromoteD
\end{zed}

\begin{schema}{Promote}
  \Delta Multi\_Task \\
  \Delta Task \\
  target?: TASK
\where
  target? \in \dom exeCore \\
  subTask(exeCore(target?)) = \theta Task \\
  subTask' = subTask \oplus \{ (exeCore(target?), \theta Task~') \} \\
  exeCore' = exeCore
\end{schema}

\begin{zproof}[Promote\$domainCheck]
 prove;
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 prove;
\end{zproof}


\begin{zed}
  SuspendTaskN\_MT \defs \exists \Delta Task @ SuspendTaskN\_T \land Promote
\end{zed}

\begin{zed}
  SuspendTaskS\_MT \defs \exists \Delta Task @ SuspendTaskS\_T \land Promote
\end{zed}

\begin{zed}
  SuspendTaskO\_MT \defs \exists \Delta Task @ SuspendTaskO\_T \land Promote
\end{zed}

\begin{zed}
  ResumeTaskN\_MT \defs \exists \Delta Task @ ResumeTaskN\_T \land Promote
\end{zed}

\begin{zed}
  ResumeTaskS\_MT \defs \exists \Delta Task @ ResumeTaskS\_T \land Promote
\end{zed}

\begin{zed}
  ChangeTaskPriorityN\_MT \defs \exists \Delta Task @ ChangeTaskPriorityN\_T \land Promote
\end{zed}

\begin{zed}
  ChangeTaskPriorityS\_MT \defs \exists \Delta Task @ ChangeTaskPriorityS\_T \land Promote
\end{zed}

\begin{zed}
  ChangeTaskPriorityD\_MT \defs \exists \Delta Task @ ChangeTaskPriorityD\_T \land Promote
\end{zed}

\begin{schema}{MigrationN\_MT}
  \Delta Multi\_Task \\
  target?: TASK \\
  topReady!: TASK \\
  newCore?: cores \\
  srcSys, tarSys: Task \\
\where
  target? \in \dom exeCore \\
  srcSys = subTask(exeCore(target?)) \\
  tarSys = subTask(newCore?) \\
  srcSys . state(target?) \in \{ ready, blocked, suspended \} \\
  srcSys . state(target?) = ready \implies srcSys . priority(target?) \leq tarSys . priority(tarSys . running\_task) \\
  target? \notin idles \\
  newCore? \neq exeCore(target?) \\
  \{ exeCore(target?), newCore? \} \ndres subTask' = \{ exeCore(target?), newCore? \} \ndres subTask \\
  \exists \Delta Task @ \\
    subTask(exeCore(target?)) = \theta Task \\
    \land DeleteTaskN\_T \\
    \land subTask'(exeCore(target?)) = \theta Task~' \\
  \exists \Delta Task; tpri: \nat | \\
    tpri = (srcSys . priority (target?)) @ \\
      subTask(newCore?) = \theta Task \\
      \land CreateTaskN\_T[tpri/newpri?] \\
      \land subTask'(newCore?) = \theta Task~' \\
  exeCore' = exeCore \oplus \{ (target?, newCore?) \}
\end{schema}

\begin{zproof}[MigrationN\_MT\$domainCheck]
 prove;
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 use applyInRanFun[cores, Task][f:= subTask, a:=exeCore(target?)];
 use applyInRanFun[cores, Task][f:= subTask, a:=newCore?]; 
 apply Task\$member to predicate subTask (exeCore~target?) \in Task;
 apply Task\$member to predicate subTask~newCore? \in Task; 
 with normalization prove; 
\end{zproof}

\begin{schema}{MigrationS\_MT}
  \Delta Multi\_Task \\
  target?: TASK \\
  topReady!: TASK \\
  newCore?: cores \\
  srcSys, tarSys: Task
\where
  target? \in \dom exeCore \\
  srcSys = subTask(exeCore(target?)) \\
  tarSys = subTask(newCore?) \\
  srcSys . state(target?) = ready \\
  srcSys . priority(target?) > tarSys . priority(tarSys . running\_task) \\
  target? \notin idles \\
  newCore? \neq exeCore(target?) \\
  \{ exeCore(target?), newCore? \} \ndres subTask' = \{ exeCore(target?), newCore? \} \ndres subTask \\
  \exists \Delta Task @ \\
    subTask(exeCore(target?)) = \theta Task \\
    \land DeleteTaskN\_T \\
    \land subTask'(exeCore(target?)) = \theta Task~' \\
  \exists \Delta Task; tpri: \nat | \\
    tpri = (srcSys . priority (target?)) @ \\
      subTask(newCore?) = \theta Task \\
      \land CreateTaskS\_T[tpri/newpri?] \\
      \land subTask'(newCore?) = \theta Task~' \\
  exeCore' = exeCore \oplus \{ (target?, newCore?) \}
\end{schema}

\begin{zproof}[MigrationS\_MT\$domainCheck]
 prove;
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 use applyInRanFun[cores, Task][f:= subTask, a:=exeCore(target?)];
 use applyInRanFun[cores, Task][f:= subTask, a:=newCore?]; 
 apply Task\$member to predicate subTask (exeCore~target?) \in Task;
 apply Task\$member to predicate subTask~newCore? \in Task; 
 with normalization prove; 
\end{zproof}

\begin{schema}{MigrationRuN\_MT}
  \Delta Multi\_Task \\
  target?: TASK \\
  topReady!: TASK \\
  newCore?: cores \\
  srcSys, tarSys: Task
\where
  target? \in \dom exeCore \\
  srcSys = subTask(exeCore(target?)) \\
  tarSys = subTask(newCore?) \\
  srcSys . state(target?) = running \\
  srcSys . priority(target?) \leq tarSys . priority(tarSys . running\_task) \\
  target? \notin idles \\
  newCore? \neq exeCore(target?) \\
  \{ exeCore(target?), newCore? \} \ndres subTask' = \{ exeCore(target?), newCore? \} \ndres subTask \\
  \exists \Delta Task @ \\
    subTask(exeCore(target?)) = \theta Task \\
    \land DeleteTaskS\_T \\
    \land subTask'(exeCore(target?)) = \theta Task~' \\
  \exists \Delta Task; tpri: \nat | \\
    tpri = (srcSys . priority (target?)) @ \\
      subTask(newCore?) = \theta Task \\
      \land CreateTaskN\_T[tpri/newpri?] \\
      \land subTask'(newCore?) = \theta Task~' \\
  exeCore' = exeCore \oplus \{ (target?, newCore?) \}
\end{schema}

\begin{zproof}[MigrationRuN\_MT\$domainCheck]
 prove;
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 use applyInRanFun[cores, Task][f:= subTask, a:=exeCore(target?)];
 use applyInRanFun[cores, Task][f:= subTask, a:=newCore?]; 
 apply Task\$member to predicate subTask (exeCore~target?) \in Task;
 apply Task\$member to predicate subTask~newCore? \in Task; 
 with normalization prove; 
\end{zproof}

\begin{schema}{MigrationRuS\_MT}
  \Delta Multi\_Task \\
  target?: TASK \\
  topReady!: TASK \\
  newCore?: cores \\
  srcSys, tarSys: Task
\where
  target? \in \dom exeCore \\
  srcSys = subTask(exeCore(target?)) \\
  tarSys = subTask(newCore?) \\
  srcSys . state(target?) = running \\
  srcSys . priority(target?) > tarSys . priority(tarSys . running\_task) \\
  target? \notin idles \\
  newCore? \neq exeCore(target?) \\
  \{ exeCore(target?), newCore? \} \ndres subTask' = \{ exeCore(target?), newCore? \} \ndres subTask \\
  \exists \Delta Task @ \\
    subTask(exeCore(target?)) = \theta Task \\
    \land DeleteTaskS\_T \\
    \land subTask'(exeCore(target?)) = \theta Task~' \\
  \exists \Delta Task; tpri: \nat | \\
    tpri = (srcSys . priority (target?)) @ \\
      subTask(newCore?) = \theta Task \\
      \land CreateTaskS\_T[tpri/newpri?] \\
      \land subTask'(newCore?) = \theta Task~' \\
  exeCore' = exeCore \oplus \{ (target?, newCore?) \}
\end{schema}

\begin{zproof}[MigrationRuS\_MT\$domainCheck]
 prove;
 invoke \Delta Multi\_Task;
 invoke predicate Multi\_Task;
 use applyInRanPfun[TASK, CORE][A:= TASK, B:= cores, f:= exeCore, a:= target?];
 use applyInRanFun[cores, Task][f:= subTask, a:=exeCore(target?)];
 use applyInRanFun[cores, Task][f:= subTask, a:=newCore?]; 
 apply Task\$member to predicate subTask (exeCore~target?) \in Task;
 apply Task\$member to predicate subTask~newCore? \in Task; 
 with normalization prove; 
\end{zproof}



\begin{zed}
  CN\_T \defs CreateTaskN\_T
\end{zed}

\begin{zed}
  CS\_T \defs CreateTaskS\_T
\end{zed}

\begin{zed}
  DN\_T \defs DeleteTaskN\_T
\end{zed}

\begin{zed}
  DS\_T \defs DeleteTaskS\_T
\end{zed}

\begin{zed}
  SN\_T \defs SuspendTaskN\_T
\end{zed}

\begin{zed}
  SS\_T \defs SuspendTaskS\_T
\end{zed}

\begin{zed}
  SO\_T \defs SuspendTaskO\_T
\end{zed}

\begin{zed}
  RN\_T \defs ResumeTaskN\_T
\end{zed}

\begin{zed}
  RS\_T \defs ResumeTaskS\_T
\end{zed}

\begin{zed}
  ChN\_T \defs ChangeTaskPriorityN\_T
\end{zed}

\begin{zed}
  ChS\_T \defs ChangeTaskPriorityS\_T
\end{zed}

\begin{zed}
  ChD\_T \defs ChangeTaskPriorityD\_T
\end{zed}

\begin{schema}{getRunningTask}
  \Xi Multi\_Task \\
  core?: cores \\
  RT!: TASK
\where
  RT! = (subTask(core?)) . running\_task
\end{schema}

\begin{zproof}[getRunningTask\$domainCheck]
  prove;
\end{zproof}

\begin{schema}{getPriority}
  \Xi Multi\_Task \\
  task?: TASK \\
  PRIORITY!: \nat
\where
  \exists core: cores | task? \in (subTask(core)) . tasks \\
    @ PRIORITY! = (subTask(core)) . priority(task?)
\end{schema}

\begin{zproof}[getPriority\$domainCheck]
  prove by reduce;
  use applyInRanFun[cores, Task][f:=subTask, a:=core]; 
  apply Task$member to predicate subTask~core \in Task;
  prove;
\end{zproof}





\end{document}
